home *** CD-ROM | disk | FTP | other *** search
/ TeX 1995 July / TeX CD-ROM July 1995 (Disc 1)(Walnut Creek)(1995).ISO / macros / latex209 / contrib / vdm / vdm.sty (.txt) < prev    next >
LaTeX Document  |  1993-11-07  |  44KB  |  1,128 lines
  1. %%% ====================================================================
  2. %%%  @LaTeX-style-file{
  3. %%%     author          = "Mario Wolczko",
  4. %%%     version         = "3.01",
  5. %%%     date            = "21 May 1992",
  6. %%%     time            = "21:05:48 BST",
  7. %%%     filename        = "vdm.sty",
  8. %%%     address         = "Dept of Computer Science
  9. %%%                        The University of Manchester
  10. %%%                        Oxford Road
  11. %%%                        Manchester M13 9PL
  12. %%%                        UK",
  13. %%%     telephone       = "+44-61-275-6146",
  14. %%%     FAX             = "+44-61-275-6236",
  15. %%%     checksum        = "32169 1413 3689 43831",
  16. %%%     email           = "mario@cs.man.ac.uk (Internet)",
  17. %%%     codetable       = "ISO/ASCII",
  18. %%%     keywords        = "LaTeX, VDM specification language",
  19. %%%     supported       = "yes",
  20. %%%     docstring       = "LaTeX macros for typesetting VDM
  21. %%%     specifications.",
  22. %%%  }
  23. %%% ====================================================================
  24. %    BSI VDM documentstyle option for LaTeX
  25. %    M. Wolczko
  26. % Last edited: Thu May 21 21:05:52 1992 by mario (Mario Wolczko) on madarch
  27. % Dept. of Computer Science   Internet:      mario@cs.man.ac.uk
  28. % The University              uucp:    mcsun!uknet!man.cs!mario
  29. % Manchester M13 9PL          JANET:         mario@uk.ac.man.cs
  30. % U.K.                        Tel: +44-61-275 6146  (FAX: 6236)
  31. %    Can use either the AMS ms[ab]m fonts or the MoreMath font if
  32. %    available: follow the instructions near the string FONT-CUSTOMIZING.
  33. %----------------------------------------------------------------
  34. %    Installation-dependent features
  35. \let\vdm\relax % signal to ps-amsfonts
  36. \newif\ifams@% use AMS fonts?
  37. \newif\ifps@ % PostScript-based?
  38. \newif\ifmoremath@ % use MoreMath font?
  39. \newif\ifnfss@ % NFSS?
  40. % NFSS code is enabled if \selectfont is defined;
  41. % this is the usual test for the nfss.
  42. \ifx\selectfont\@undefined
  43.  \global\nfss@false
  44. \else
  45.  \global\nfss@true
  46. \ifnfss@
  47.   % This is a patch for an NFSS bug, from Frank Mittelbach.
  48.   % It applies to the versions of lfonts.new of NFSS up to
  49.   %\def\fileversion{v1.3a}
  50.   %\def\filedate{91/11/27}
  51.   %\def\docdate {90/01/28}
  52.   \def\extract@alph@from@version#1#2{%
  53.     % #1 = alph id (cs)
  54.     % #2 = version (string)
  55.     \expandafter\extract@alph@from@version@\expandafter
  56.     #1\csname mv@#2\endcsname}
  57.   \def\extract@alph@from@version@#1#2{%
  58.     % #1 = alph id (cs)
  59.     % #2 = version (cs)
  60.     \def\extract@help##1\gdef#1##2##3\@nil{%
  61.       \def\@tempa####1{\gdef#2{##1####1##3}}%
  62.       \def\content@part{##2}}%
  63.     \expandafter\extract@help#2\@nil
  64.     \def\extract@group@no@etc\select@group#1##1##2##3\@nil{%
  65.       % ##1 group no
  66.       % ##2 extra part
  67.       % ##3 fam/ser/sha
  68.       \@tempa{%
  69.     \getanddefine@fonts{##1}##3%
  70.     \gdef#1{\use@mathgroup##2{##1}}}}%
  71.     \expandafter\extract@group@no@etc\content@part\@nil}
  72.   \def\select@group#1#2#3#4{\relax \ifmmode
  73.     \begingroup
  74.       \let \math@fonts \@empty
  75.       \escapechar \m@ne
  76.       \getanddefine@fonts #2#4%
  77.       \globaldefs \@ne
  78.       \math@fonts
  79.     \endgroup
  80.     \gdef #1{\use@mathgroup #3{#2}}%
  81.     \expandafter\extract@alph@from@version
  82.       \expandafter#1\expandafter{\math@version}%
  83.     \expandafter #1\fi }
  84. \def\@fmtname{lplain}
  85. \def\@psfmtname{pslplain}
  86. \def\@testcmsy{\if@usecmsy \else
  87.   \@latexerr{Can't use vdm with this PSLaTeX}%
  88.     {This PSLaTeX does not have the CMSY symbols
  89.     available, and cannot be used with VDM style.  Get
  90.     a guru to rebuild PSLaTeX with the CMSY and CMMI
  91.     fonts included.}\fi}
  92. \def\@testcmmi{\if@usecmmi \else
  93.   \@latexerr{Can't use vdm with this PSLaTeX}%
  94.     {This PSLaTeX does not have the CMMI symbols
  95.     available, and cannot be used with VDM style.  Get
  96.     a guru to rebuild PSLaTeX with the CMSY and CMMI
  97.     fonts included.}\fi}
  98. \global\ps@false
  99. \ifx\fmtname\@psfmtname
  100.   \global\ps@true \@testcmsy \@testcmmi
  101. % FONT-CUSTOMIZING
  102. % Decide under which conditions, you want to use which fonts.
  103. % You need to set either ams@true or ams@false, and either moremath@true or
  104. % moremath@false.
  105. % If in doubt, set both to false.
  106. % This uses moremath if pslatex/NFSS is in use , AMS fonts otherwise.
  107. \global\moremath@false \global\ams@true
  108. \ifps@
  109.   \ifnfss@ \global\moremath@true \global\ams@false \fi
  110. \else\ifx\fmtname\@fmtname
  111. \else \global\ams@false % don't use AMS for SliTeX
  112. \fi\fi
  113. \ifnfss@
  114.   \ifams@
  115.      % Firstly we call amsfonts.sty to load the AMS fonts for us.
  116.      \ifps@
  117.        \input ps-amsfonts.sty
  118.      \else
  119.        \input amsfonts.sty
  120.      \fi
  121.      \edef\msx@{\hexnumber@\msa@group}
  122.      \edef\msy@{\hexnumber@\msb@group}
  123.   \else\ifmoremath@
  124.      \new@mathgroup\mm@group
  125.      \define@mathgroup\mv@normal\mm@group{mm}{m}{n}
  126.      \edef\mm@{\hexnumber@\mm@group}
  127.      % FONT-CUSTOMIZING
  128.      % substitute correct name of MoreMath font here
  129.      \new@fontshape{mm}{m}{n}{%
  130.     <5>pmmr at5pt%
  131.     <6>pmmr at6pt%
  132.     <7>pmmr at7pt%
  133.     <8>pmmr at8pt%
  134.     <9>pmmr at9pt%
  135.     <10>pmmr at10pt%
  136.     <11>pmmr at10.95pt%
  137.     <12>pmmr at12pt%
  138.     <14>pmmr at14.4pt%
  139.     <17>pmmr at17.28pt%
  140.     <20>pmmr at20.74pt%
  141.     <25>pmmr at24.88pt}{}
  142.      \extra@def{mm}{}{}
  143.   \fi\fi
  144.   % \itfam is only defined if oldlfonts is in force, so if it is not defined,
  145.   % define it.
  146.   \ifx\itfam\@undefined
  147.     \new@mathgroup\itfam
  148.     \ifps@
  149.       \new@internalmathalphabet\mathit\itfam{times}{m}{it}
  150.     \else
  151.       \new@internalmathalphabet\mathit\itfam{cmr}{m}{it}
  152.     \fi
  153.   \fi
  154.   \ifx\math@bgroup\@empty
  155.      % nomargid synatax, \mathit will just switch the \fam if the font is
  156.      % already loaded, but will load the font the first time.
  157.      \def\vdm@it{\mathit}
  158.   \else
  159.      % margid syntax, as for nomargid, but here the scope of \mathit is its
  160.      % argument, so we call it with a null argument to make sure the font is
  161.      % loaded, then switch \fam in the old way.
  162.      \def\vdm@it{\mathit{}\fam\itfam}
  163.   \fi
  164. \else
  165.   \ifams@
  166.     % kludges for \newfam necessary because it's \outer
  167.     \csname newfam\endcsname\msxfam
  168.       \csname newfam\endcsname\msyfam
  169.     % this is lifted from amssymbols.sty
  170.     \ifcase\@ptsize
  171.      \font\tenmsx=msam10
  172.      \font\sevenmsx=msam7
  173.      \font\fivemsx=msam5
  174.      \font\tenmsy=msbm10
  175.      \font\sevenmsy=msbm7
  176.      \font\fivemsy=msbm5
  177.      \font\tenmsx=msam10 scaled \magstephalf
  178.      \font\sevenmsx=msam8
  179.      \font\fivemsx=msam5 scaled \magstephalf
  180.      \font\tenmsy=msbm10 scaled \magstephalf
  181.      \font\sevenmsy=msbm8
  182.      \font\fivemsy=msbm5 scaled \magstephalf
  183.      \font\tenmsx=msam10 scaled \magstep1
  184.      \font\sevenmsx=msam8
  185.      \font\fivemsx=msam5 scaled \magstephalf
  186.      \font\tenmsy=msbm10 scaled \magstep1
  187.      \font\sevenmsy=msbm8
  188.      \font\fivemsy=msbm5 scaled \magstephalf
  189.     \textfont\msxfam=\tenmsx  \scriptfont\msxfam=\sevenmsx
  190.       \scriptscriptfont\msxfam=\fivemsx
  191.     \textfont\msyfam=\tenmsy  \scriptfont\msyfam=\sevenmsy
  192.       \scriptscriptfont\msyfam=\fivemsy
  193.     \def\hexnumber@#1{\ifnum#1<10 \number#1\else
  194.      \ifnum#1=10 A\else\ifnum#1=11 B\else\ifnum#1=12 C\else
  195.      \ifnum#1=13 D\else\ifnum#1=14 E\else
  196.      \ifnum#1=15 F\fi\fi\fi\fi\fi\fi\fi}
  197.     \def\msx@{\hexnumber@\msxfam}
  198.     \def\msy@{\hexnumber@\msyfam}
  199.   \else\ifmoremath@
  200.       \csname newfam\endcsname\mmfam
  201.          \edef\mm@{\hexnumber@\mmfam}
  202.   \else\fi
  203.   \fi
  204.   % NFSS-change
  205.   % The previous version placed \fam\itfam in \everymath to get text italic
  206.   % in math mode. This does not work if this font has not yet been loaded.
  207.   % With oldlatex, most text italic sizes are preloaded, but \huge\it may not
  208.   % be.
  209.   % With the nfss, things may be set up so almost no fonts are preloaded.
  210.   % we will put \vdm@it into \everymath later, here we give the definition
  211.   % for oldlatex, \fam\itfam as before.
  212.   \def\vdm@it{\fam\itfam}
  213. %----------------------------------------------------------------
  214. %    The vdm environment
  215. % record whether we were in horizontal mode when entering...
  216. \newif\ifhm@
  217. \def\vdm{\ifhmode\hm@true\else\hm@false\fi
  218.   \@changeMathmodeCatcodes\@postUnderPenalty10000\relax}
  219. % after an \end{vdm} the next paragraph is not indented unless a \par
  220. % comes first (if we entered in horizontal mode).  This is a bit of a
  221. % kludge!
  222. \def\endvdm{\ifhm@\else
  223.   \global\let\par=\@undonoindent
  224.   \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
  225.             \global\let\par=\@@par}%
  226.   \fi}
  227. \def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}
  228. %-----------------------------------------------------------------
  229. %     Controlling line and page breaks
  230. % Text within the vdm environment is essentially mathematical in
  231. % nature, so requires special care.  Whenever outer vertical mode is
  232. % entered, the \@beginVerticalVDM command should be used.  This sets
  233. % up \leftskip, \rightskip, \baselineskip, \lineskip and
  234. % \lineskiplimit to conform with the overall style.
  235. % When entering unrestricted horizontal mode, the \@beginHorizontalVDM
  236. % command should be used.  This sets up:
  237. %    \leftskip and \rightskip to 0,
  238. %    \\ to do line breaking
  239. %    ragged right line breaking, with special penalties, and
  240. %    enters math mode.
  241. % \@endHorizontalVDM should be called when leaving unrestricted
  242. % horizontal mode.
  243. \def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}
  244. \def\@beginHorizontalVDM{\@restoreLineSeparator
  245.   \@restoreMargins\@raggedRight\noindent$\strut\relax}
  246. \def\@endHorizontalVDM{\relax\strut$}
  247. % \VDMindent is used for \leftskip within VDM, \VDMrindent for
  248. % \rightskip, \VDMbaselineskip for \baselineskip
  249. \newdimen\VDMindent \VDMindent=\parindent
  250. \newdimen\VDMrindent \VDMrindent=\parindent
  251. \def\VDMbaselineskip{\baselineskip}
  252. \def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
  253. \def\@restoreMargins{\advance\hsize by-\leftskip
  254.   \advance\hsize by-\rightskip
  255.   \leftskip=0pt \rightskip=0pt}
  256. \def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
  257.   \lineskip=0pt \lineskiplimit=0pt
  258.   % need to alter the size of struts, too
  259.   \setbox\strutbox\hbox{\vrule height.7\baselineskip
  260.       depth.3\baselineskip width\z@}}
  261. % these are used in externals, records and cases
  262. \def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
  263. \def\@restoreLineSeparator{\let\\=\newline}
  264. \def\@raggedRight{\rightskip=0pt plus 1fil
  265.   \hyphenpenalty=-100 \linepenalty=200
  266.   \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}
  267. %------------------------------------------------------------------------
  268. %    Font and Character Changes
  269. % make a-zA-Z use the \it family within math mode, and ~ mean \hook.
  270. % Digits 0-9 remain as normal.
  271. \everymath=\expandafter{\the\everymath\vdm@it
  272.     \@changeMathmodeCatcodes}
  273. \everydisplay=\expandafter{\the\everydisplay\vdm@it
  274.     \@changeMathmodeCatcodes}
  275. \mathcode`\0="0030
  276. \mathcode`\1="0031
  277. \mathcode`\2="0032
  278. \mathcode`\3="0033
  279. \mathcode`\4="0034
  280. \mathcode`\5="0035
  281. \mathcode`\6="0036
  282. \mathcode`\7="0037
  283. \mathcode`\8="0038
  284. \mathcode`\9="0039
  285. % If the user really wants the normal codes, she can call \defaultMathcodes
  286. \def\defaultMathcodes{\let\vdm@it\relax}
  287. % remember the original mathcode of minus sign
  288. \edef\@minuscode{\the\mathcode`\-}
  289. \def\mathminus{\mathcode`\-=\@minuscode }
  290. \def\textminus{\mathcode`\-="002D }
  291. % by default, use text minus
  292. %\textminus
  293. % make a : into punctuation, a - into a letter, and | mean \mid
  294. \ifps@
  295.  \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
  296.   \mathcode`\|="327C \mathchardef\Or="32DA % this is a rel to get 5mu spacing
  297.   \mathcode`\f="0166} % normal letter spacing
  298. \else
  299.  % NFSS-change
  300.  % \mathcode`\-="042D changed to \mathcode`\-="002D as we can not rely on
  301.  % \itfam being fam 4.
  302.  \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
  303.   \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
  304.  \def\relbar{\mathrel{\smash\minus}}% redefine because mathcode of -
  305.                     % has changed
  306. % alternative underscore
  307. \def\@VDMunderscore{\leavevmode
  308.   \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
  309.   \hskip 0.1em}
  310. % Allow line breaks after an underscore, but not in vdm mode (see
  311. % \vdm).  This is so long identifiers can be broken when run
  312. % into paragraphs.
  313. \newcount\@postUnderPenalty \@postUnderPenalty=200
  314. % now require some catcode trickery to enable us to change _ when we want to
  315. {\catcode`\_=\active \catcode`\"=\active
  316.  \gdef\@changeGlobalCatcodes{% make _ a normal char
  317.     \catcode`\_=\active \let_=\@VDMunderscore}
  318.  \gdef\@changeMathmodeCatcodes{%
  319.     % make ~ mean \hook, " do text, @ mean subscript
  320.     \let~=\hook
  321.     \catcode`\@=8
  322.     \catcode`\"=\active  \let"=\@mathText}
  323.  \gdef\underscoreoff{% make _ a normal char
  324.     \catcode`\_=\active \let_=\@VDMunderscore}
  325.  \gdef\underscoreon{% restore underscore to usual meaning
  326.     \catcode`\_=8}
  327.  \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
  328. \ifnfss@
  329.   \def\mathTextFont{\mathrm}
  330. \else
  331.   \def\mathTextFont{\rm}
  332. %----------------------------------------------------------------
  333. %    Keywords
  334. \ifx\fmtname\@fmtname
  335.     \def\keywordFontBeginSequence{\sf}%    user-definable
  336. \else\ifx\fmtname\@psfmtname
  337.     \def\keywordFontBeginSequence{\sf}% Helvetica is OK
  338. \else
  339.     \def\keywordFontBeginSequence{\bf}% good for SliTeX
  340. \fi\fi
  341. \def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}
  342. \def\makeNewKeyword#1#2{% use \newcommand for extra checks
  343.     \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}
  344. \makeNewKeyword{\nil}{nil}
  345. \makeNewKeyword{\True}{true}
  346. \makeNewKeyword{\true}{true}
  347. \makeNewKeyword{\False}{false}
  348. \makeNewKeyword{\false}{false}
  349. \makeNewKeyword{\rem}{ rem }
  350. \def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}
  351. %----------------------------------------------------------------
  352. %    monadic operator creation
  353. \def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}
  354. %----------------------------------------------------------------
  355. %    primitive numeric types
  356. % use the AMS fonts for these if possible
  357. \ifams@
  358.   \mathchardef\Bool="0\msy@42    % Booleans
  359.   \mathchardef\Nat="0\msy@4E    % Natural numbers
  360.   \def\Nati{\Nat_1}        % Positive natural numbers
  361.   \mathchardef\Int="0\msy@5A    % Integers
  362.   \mathchardef\Real="0\msy@52    % Reals
  363.   \mathchardef\Rat="0\msy@51    % Rationals
  364. \else\ifmoremath@
  365.   \mathchardef\Bool="0\mm@42    % Booleans
  366.   \mathchardef\Nat="0\mm@4E    % Natural numbers
  367.   \def\Nati{\Nat_1}        % Positive natural numbers
  368.   \mathchardef\Int="0\mm@5A    % Integers
  369.   \mathchardef\Real="0\mm@52    % Reals
  370.   \mathchardef\Rat="0\mm@51    % Rationals
  371. \else
  372.   \def\Bool{\hbox{\bf B\/}}
  373.   \def\Nat{\hbox{\bf N\/}}
  374.   \def\Nati{\hbox{$\hbox{\bf N}_1$}}
  375.   \def\Int{\hbox{\bf Z\/}}
  376.   \def\Real{\hbox{\bf R\/}}
  377.   \def\Rat{\hbox{\bf Q\/}}
  378. \fi\fi
  379. \let\Natone=\Nati % just for an alternative
  380. %----------------------------------------------------------------
  381. %    Operations
  382. % The op environment.  Within op you can specify args,
  383. % result, etc. which are gathered into registers, and output when the
  384. % op env. ends.
  385. % The optional argument is the operation name
  386. % shorthand for an operation on its own: the vdmop env.
  387. \def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}
  388. % registers constructed within an op environment
  389. \newtoks\@operationName
  390. \newbox\@operationNameBox
  391. \newif\ifArgumentListEncountered@
  392. \newtoks\@argumentListTokens
  393. \newtoks\@resultNameAndTypeTokens
  394. \newbox\@externalsBox
  395. \newbox\@preConditionBox
  396. \newbox\@postConditionBox
  397. \newbox\@errConditionBox
  398. \def\op{% clear temporaries, deal with optional arg
  399.     \setbox\@operationNameBox=\hbox{}%
  400.     \@argumentListTokens={}\ArgumentListEncountered@false
  401.     \@resultNameAndTypeTokens={}%
  402.     \setbox\@externalsBox=\box\voidb@x
  403.     \setbox\@preConditionBox=\box\voidb@x
  404.     \setbox\@postConditionBox=\box\voidb@x
  405.     \par\preOperationHook
  406.     \vskip\preOperationSkip
  407.     \@beginVerticalVDM
  408.     \@ifnextchar [{\@opname}{}}
  409. % breaking parameters
  410. \newcount\preOperationPenalty \preOperationPenalty=0
  411. \newcount\preExternalPenalty \preExternalPenalty=2000
  412. \newcount\prePreConditionPenalty \prePreConditionPenalty=800
  413. \newcount\prePostConditionPenalty \prePostConditionPenalty=500
  414. \newcount\preErrConditionPenalty \preErrConditionPenalty=500
  415. \newcount\postOperationPenalty \postOperationPenalty=-500
  416. % gaps between bits of operations
  417. \newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
  418. \newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
  419. \newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
  420. \newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
  421. \newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
  422. \newskip\preErrConditionSkip \preErrConditionSkip=.5ex plus .2ex minus .2ex
  423. \def\endop{% make up operation
  424.     % IMPORTANT---don't remove the vskips in this macro
  425.     % if you don't want one, set it to 0pt
  426.     \vskip 0pt
  427.     \@setOperationHeader
  428.     \betweenHeaderAndExternalsHook
  429.     \vskip\postHeaderSkip
  430.     \ifvoid\@externalsBox
  431.           \betweenExternalsAndPreConditionHook
  432.     \else \moveright\VDMindent\box\@externalsBox
  433.           \betweenExternalsAndPreConditionHook
  434.           \vskip\postExternalsSkip
  435.     \ifvoid\@preConditionBox
  436.           \betweenPreAndPostConditionHook
  437.     \else \moveright\VDMindent\box\@preConditionBox
  438.           \betweenPreAndPostConditionHook
  439.           \vskip\postPreConditionSkip
  440.     \ifvoid\@postConditionBox
  441.           \betweenPostAndErrHook
  442.     \else \moveright\VDMindent\box\@postConditionBox
  443.           \betweenPostAndErrConditionHook
  444.     \ifvoid\@errConditionBox
  445.     \else \vskip\preErrConditionSkip
  446.           \moveright\VDMindent\box\@errConditionBox
  447.         \postOperationHook
  448.         \vskip\postOperationSkip}
  449. % hooks for user-defined expansion
  450. % TeX is in outer vertical mode when these are called.
  451. % ALWAYS leave TeX in vertical mode after these macros have been called
  452. \def\preOperationHook{\penalty\preOperationPenalty }
  453. \def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
  454. \def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
  455. \def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
  456. \def\betweenPostAndErrConditionHook{\penalty\preErrConditionPenalty }
  457. \def\postOperationHook{\penalty\postOperationPenalty }
  458. % combine the operation name, argument list and result
  459. \def\@setOperationHeader{%
  460.     \moveright\VDMindent\vtop{%
  461.         \ifArgumentListEncountered@
  462.             \setbox\@operationNameBox=%
  463.                 \hbox{\unhbox\@operationNameBox$($}\fi
  464.         \hangindent=\wd\@operationNameBox \hangafter=1
  465.         \noindent\kern-.05em\box\@operationNameBox
  466.         \@beginHorizontalVDM
  467.         \ifArgumentListEncountered@\the\@argumentListTokens)\fi
  468.         \ \the\@resultNameAndTypeTokens
  469.         \@endHorizontalVDM}}
  470. % set the operation name
  471. % \opname{name-of-operation}
  472. \def\opname#1{\@opname[#1]}
  473. \def\@opname[#1]{\@operationName={#1}%
  474.   \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}
  475. % set up the argument list
  476. % \args{ argument \\ argument \\ argument... } where \\ forces a line break
  477. % This is also used in the fn environment
  478. \def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}
  479. % result name and type
  480. \def\res{\global\@resultNameAndTypeTokens=}
  481. % externals list
  482. % An external list could be either very long or very short, so we provide
  483. % two forms.  One is the short \ext{..} command, the other is the externals
  484. % environment.
  485. % Externals are always separated by \\
  486. % we have to mess a little to get the catcode of : right
  487. \def\ext{\bgroup\@makeColonActive\@ext}
  488. \def\@ext#1{\externals#1\endexternals\egroup}
  489. \def\externals{\global\setbox\@externalsBox=%
  490.     \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
  491. \def\endexternals{\@endIndentedPara{\@endAlignment}}
  492. \def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}
  493. % more catcode trickery for :
  494. {\catcode`\:=\active
  495.  \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}
  496. % the \expandafters are necessary because TeX doesn't expand
  497. % \halign specs when scanning for # and &
  498. \def\@beginAlignment{\expandafter\halign\expandafter\bgroup
  499.     \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
  500. \def\@endAlignment{\crcr\egroup}
  501. % the user can decide on the exact alignment of the field names
  502. \newtoks\@extAlign
  503. \def\leftExternals{\@extAlign={$##$\hfil}}
  504. \def\rightExternals{\@extAlign={\hfil$##$}}
  505. \leftExternals
  506. \makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }
  507. % pre-condition, post-condition and err-condition
  508. % once again we provide short forms \pre, \post, \err and environments
  509. % precond, postcond and errcond
  510. \def\pre#1{\precond#1\endprecond}
  511. \def\precond{\global\setbox\@preConditionBox=%
  512.     \@beginMathIndentedPara{\hsize}{pre }}
  513. \def\endprecond{\@endMathIndentedPara}
  514. \def\post#1{\postcond#1\endpostcond}
  515. \def\postcond{\global\setbox\@postConditionBox=%
  516.     \@beginMathIndentedPara{\hsize}{post }}
  517. \def\endpostcond{\@endMathIndentedPara}
  518. \def\err#1{\errcond#1\enderrcond}
  519. \def\errcond{\global\setbox\@errConditionBox=%
  520.     \@beginMathIndentedPara{\hsize}{errs }}
  521. \def\enderrcond{\@endMathIndentedPara}
  522. %----------------------------------------------------------------
  523. %    Box man\oe uvres
  524. % Here's where all the tricky box manipulation commands go
  525. % \@beginIndentedPara begins construction of a \hbox of width #1
  526. % which contains keyword #2 to the left of a para in a vtop.
  527. % #3 is evaluated within the inner vtop.
  528. % endIndentedPara closes the box off; its arg. is evaluated just
  529. % before closing the box.
  530. \def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
  531.     \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
  532. \def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}
  533. % \@beginMathIndentedPara places the para in vdm mode
  534. \def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
  535.     {\@beginHorizontalVDM}}
  536. \def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}
  537. % \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
  538. \def\@belowAndIndent#1#2{#1\hfil\break
  539.     \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}
  540. % \@mathIndentedPara does the whole thing
  541. \def\@mathIndentedPara#1#2#3{\@beginMathIndentedPara{#1}{#2}#3%
  542.     \@endMathIndentedPara}
  543. %----------------------------------------------------------------
  544. %    Constructions
  545. % Here are all the standard constructions.
  546. % The only tricky one is \cases.
  547. % Those that construct a box must be made to make that box of 0 width,
  548. % and force a line break immediately afterwards.
  549. % \If mm-exp \Then mm-exp \Else mm-exp \Fi
  550. % multi-line indented if-then-else
  551. \def\If#1\Then#2\Else#3\Fi{\vtop{%
  552.     \@mathIndentedPara{0pt}{if }{#1}%
  553.     \@mathIndentedPara{0pt}{then }{#2}%
  554.     \@mathIndentedPara{0pt}{else }{#3}}}
  555. % \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
  556. % single line if-then-else
  557. \def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  558.     \kw{if }\nobreak#1\penalty0\hskip 0.5em
  559.     \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
  560.     \kw{else }\nobreak#3\@endHorizontalVDM}\hss}}
  561. % \Let mm-exp \In mm-exp2
  562. % multi-line let..in ; mm-exp2 is `curried'
  563. \def\Let#1\In{\vtop{%
  564.     \@mathIndentedPara{0pt}{let }{#1\hskip 0.5em\kw{in}}}\hfil\break}
  565. % \SLet mm-exp \In mm-exp
  566. % single-line let..in
  567. \def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
  568.     \kw{let }\nobreak#1\hskip 0.5em
  569.     \kw{in }\penalty-100 #2\@endHorizontalVDM}\hss}}
  570. % multi-line cases
  571. % \Cases{ selecting-mm-exp }
  572. % from-case1 & to-case1 \\
  573. % from-case2 & to-case2 \\
  574. %        ...
  575. % from-casen & to-casen
  576. % \Otherwise{ mm-exp }
  577. % \Endcases[optional text for the rest of the line]
  578. \newif\ifOtherwiseEncountered@
  579. \newtoks\@OtherwiseTokens
  580. \def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
  581.         \@mathIndentedPara{\hsize}{cases }{\strut
  582.             #1\hskip 0.5em\strut\kw{of}}%
  583.         \bgroup % we might be in a nested case, so we have to
  584.             % save the \Otherwise bits we might lose
  585.         \OtherwiseEncountered@false \@changeLineSeparator
  586.         \@beginCasesAlignment}
  587. % the user can decide on the exact alignment
  588. \newtoks\@casesDef
  589. \def\leftCases{\@casesDef={$##$\hfil}}
  590. \def\rightCases{\@casesDef={\hfil$##$}}
  591. \rightCases
  592. % the \expandafters are necessary because TeX doesn't expand
  593. % \halign specs when scanning for # and &
  594. \def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
  595.     \the\@casesDef&$\,\rightarrow##$\hfil\cr}
  596. \def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
  597. \let\Others=\Otherwise
  598. \def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
  599. \def\@endCasesAlignment{\crcr\egroup}
  600. \def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
  601.     \@mathIndentedPara{\hsize}{others }{%
  602.         \strut\the\@OtherwiseTokens\strut}
  603.     \fi}
  604. % must test for the optional arg to follow the end
  605. \def\@setEndcases{\noindent
  606.     \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
  607. \def\@unbracket[#1]{$#1$\@finalCaseEnd}
  608. \def\@finalCaseEnd{\egroup\hss\egroup}%\hfil\break
  609. %----------------------------------------------------------------
  610. %    special symbols
  611. % defined as
  612. \ifps@
  613.  \def\DEF{\raise.5ex
  614.     \hbox{\footnotesize\underline{$\mathchar"3\cmsy@34$}}}% a \triangle
  615. \else
  616.  \def\DEF{\raise.5ex
  617.     \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle
  618. % cross product
  619. \let\x=\times
  620. %    logical connectives
  621. \def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
  622.     \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
  623. \let\iff=\Iff
  624. \def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
  625.     \mskip 6mu plus 2mu minus 1mu}
  626. \let\implies=\Implies
  627. % see changeOtherMathcodes for \Or
  628. \let\And=\land
  629. \let\@and=\and
  630. \def\and{\ifmmode\And\else\@and\fi}
  631. %  use \neg for logical not, or
  632. \def\Not{\neg\,}
  633. %    quantification
  634. \ifps@
  635.  \mathchardef\Exists="0224
  636.  \mathchardef\Forall="0222
  637.  \mathchardef\suchthat="22D7
  638. \else
  639.  \mathchardef\Exists="0239
  640.  \mathchardef\Forall="0238
  641.  \mathchardef\suchthat="2201
  642. \def\exists{\@ifstar{\@splitExists}{\@normalExists}}
  643. \ifams@
  644.   \mathchardef\@nexists="0\msy@40 % crossed out existential quantifier
  645. \else\ifps@
  646.   \def\@nexists{\hbox to 0pt{\kern0.2ex\raise0.1ex\hbox{/}\hss}\Exists}
  647. \else
  648.   \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
  649. \fi\fi
  650. \def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
  651. \def\forall{\@ifstar{\@splitForall}{\@normalForall}}
  652. \def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
  653. \def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}
  654. \def\@normalExists#1#2{{\Exists#1}\suchthat #2}
  655. \def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
  656. \def\@normalForall#1#2{{\Forall#1}\suchthat #2}
  657. \def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
  658. \def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}
  659. \def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
  660. \def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
  661. \def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
  662. \def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
  663. \def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
  664. %    sequents
  665. \let\Tstlp=\vdash
  666. \def\sequent{\@ifstar{\@splitSequent}{\@normalSequent}}
  667. \def\@normalSequent#1#2{{#1}\:\Tstlp\: #2}
  668. \def\@splitSequent#1{\@belowAndIndent{#1\;\Tstlp}}
  669. %    strachey brackets
  670. % (see TeXbook, p.437)
  671. \ifmoremath@
  672.   \def\term#1{\thinspace\mathchar"4\mm@ D2\relax#1\mathchar"5\mm@ D4\thinspace}
  673. \else
  674.   \def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}
  675. %    function composition
  676. \let\compf=\circ
  677. %----------------------------------------------------------------
  678. %    function environment
  679. % This environment is similar to the op environment, but is used for
  680. % function definition.
  681. % The mandatory first parameter is the name of the function, the
  682. % second is the argument list.
  683. % The *-form simply doesn't force the parentheses round the argument list
  684. \def\fn{\parens@true\@beginVDMfunction}
  685. \@namedef{fn*}{\parens@false\@beginVDMfunction}
  686. \@namedef{endfn*}{\endfn}
  687. % short form
  688. \def\vdmfn{\vdm\parens@true \@beginVDMfunction}
  689. \def\endvdmfn{\endfn\endvdm}
  690. \@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
  691. \@namedef{endvdmfn*}{\endfn\endvdm}
  692. % registers used within the fn environment
  693. \newtoks\@fnName
  694. \newbox\@fnNameBox
  695. \newif\ifsignatureEncountered@
  696. \newtoks\@signatureTokens
  697. \newbox\@fnDefnBox
  698. \newif\ifparens@
  699. \def\@beginVDMfunction#1#2{%
  700.     \@fnName={#1}%
  701.     \setbox\@fnNameBox=\hbox{$#1$}%
  702.     \setbox\@preConditionBox=\box\voidb@x % for people who want to do
  703.     \setbox\@postConditionBox=\box\voidb@x% implicit defns
  704.     \@signatureTokens={}\signatureEncountered@false
  705.     \ifparens@
  706.         \@argumentListTokens={(#2)}%
  707.     \else
  708.         \@argumentListTokens={#2}%
  709.     \par\preFunctionHook
  710.     \vskip\preFunctionSkip
  711.     \@beginVerticalVDM
  712.     \@beginFnDefn}
  713. % read in a signature
  714. \def\signature{\global\signatureEncountered@true \global\@signatureTokens=}
  715. \def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
  716.     \hangindent=2em \hangafter=1 \@beginHorizontalVDM
  717.     \advance\hsize by-2em % this fools vboxes within the
  718.     % function body about the hanging indent...yuk.
  719.     % If you change the size of the indent, change the
  720.     % corresponding line in \endfn.
  721.     \copy\@fnNameBox \the\@argumentListTokens
  722.     \quad\DEF\penalty-100\quad }
  723. \newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
  724. \newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
  725. \newskip\betweenSignatureAndBodySkip
  726. \betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
  727. \newskip\betweenFunctionAndPreSkip
  728. \betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex
  729. \def\endfn{%
  730.     \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
  731.     \@endHorizontalVDM
  732.     \egroup  % this ends the vtop we started in \@beginFnDefn
  733.     \ifsignatureEncountered@
  734.         \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
  735.         \dimen255=\wd0 \noindent \box0
  736.         \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
  737.             \the\@signatureTokens \@endHorizontalVDM}\par
  738.         \betweenSignatureAndBodyHook
  739.         \vskip\betweenSignatureAndBodySkip
  740.     \moveright\VDMindent\box\@fnDefnBox\,
  741.     \ifvoid\@preConditionBox
  742.           \betweenPreAndPostConditionHook
  743.           \vskip\postFunctionSkip
  744.     \else \betweenFunctionAndPreHook
  745.           \vskip\betweenFunctionAndPreSkip
  746.           \moveright\VDMindent\box\@preConditionBox
  747.           \betweenPreAndPostConditionHook
  748.           \vskip\postPreConditionSkip
  749.     \ifvoid\@postConditionBox
  750.           \postFunctionHook
  751.     \else \moveright\VDMindent\box\@postConditionBox
  752.           \postFunctionHook
  753.           \vskip\postOperationSkip
  754.     \fi}
  755. \newcount\preFunctionPenalty \preFunctionPenalty=0
  756. \newcount\betweenSignatureAndBodyPenalty
  757.  \betweenSignatureAndBodyPenalty=10000
  758. \newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
  759. \newcount\postFunctionPenalty \postFunctionPenalty=-500
  760. % These are called in outer vertical mode---they must also exit in this mode
  761. \def\preFunctionHook{\penalty\preFunctionPenalty }
  762. \def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
  763. \def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
  764. \def\postFunctionHook{\penalty\postFunctionPenalty }
  765. %    other function-related things
  766. % function arrow
  767. \def\to{\penalty-100\rightarrow}
  768. % explicit lamdba function
  769. \def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
  770. \def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
  771. \def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
  772.     {\lambda#1}\suchthat\hfil\break
  773.     \@mathIndentedPara{\hsize}{\qquad}{#2}}
  774. %----------------------------------------------------------------
  775. %    Optional fields
  776. \def\Opt#1{\big[#1\big]}
  777. %----------------------------------------------------------------
  778. %    Sets
  779. % new set type
  780. \def\setof#1{#1-\kw{set}}
  781. % set enumeration
  782. \def\set#1{\{#1\}}
  783. % empty set
  784. \def\emptyset{\{\,\}}
  785. % usual LaTeX operators apply: \in \notin \subset \subseteq
  786. \let\inter=\cap \let\intersection=\inter
  787. \let\Inter=\bigcap \let\Intersection=\Inter
  788. \let\union=\cup
  789. \let\Union=\bigcup
  790. \ifps@
  791.  \mathchardef\minus="222D
  792. \else
  793.  \mathchardef\minus="2200
  794. \def\diff{\minus} \let\difference=\diff
  795. \newMonadicOperator{\card}{card}
  796. \newMonadicOperator{\Min}{min}
  797. \newMonadicOperator{\Max}{max}
  798. \newMonadicOperator{\abs}{abs}
  799. %----------------------------------------------------------------
  800. %     Map type
  801. % new map type
  802. \def\mapof#1#2{#1\buildrel m\over\longrightarrow#2}
  803. % one-one map
  804. \def\mapinto#1#2{#1\buildrel m\over\longleftrightarrow#2}
  805. % map enumeration
  806. \def\map#1{\{#1\}}
  807. % empty map
  808. \def\emptymap{\{\,\}}
  809. %    map operators
  810. % use \mapsto for |->
  811. % overwrite
  812. \def\owr{\dagger}
  813. \ifmoremath@
  814.   \mathchardef\dres="2\mm@ B2
  815.   \mathchardef\rres="2\mm@ B3 % the right hand version
  816. \else
  817.   \let\dres=\lhd
  818.   \let\rres=\rhd
  819. % domain subtraction
  820. \ifmoremath@
  821.   \mathchardef\dsub="2\mm@ F8
  822. % what a horror -- some people will insist on these daft symbols...
  823. \else\ifps@
  824.  \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-3mu\hbox{$\dres$}$}}}
  825. \else
  826.  \def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  827.     \lower.1ex\hbox{$\dres$}$}}}
  828. \fi\fi
  829. % range subtraction
  830. \ifmoremath@
  831.   \mathchardef\rsub="2\mm@ F9
  832. \else\ifps@
  833.  \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu\rres$}}}
  834. \else
  835.  \def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
  836.     \lower.1ex\hbox{$\rres$}$}}}
  837. \fi\fi
  838. \newMonadicOperator{\dom}{dom}
  839. \newMonadicOperator{\rng}{rng}
  840. \newMonadicOperator{\merge}{merge}
  841. %----------------------------------------------------------------
  842. %    Sequences
  843. % new type
  844. \def\seqof#1{#1^*}
  845. % non-empty sequence
  846. \def\neseqof#1{#1^+}
  847. % enumeration
  848. \def\seq#1{[#1]}
  849. % empty sequence
  850. \def\emptyseq{[\,]}
  851. \newMonadicOperator{\len}{len}
  852. \newMonadicOperator{\hd}{hd}
  853. \newMonadicOperator{\tl}{tl}
  854. \newMonadicOperator{\elems}{elems}
  855. \newMonadicOperator{\inds}{inds}
  856. \def\cons#1{\kw{cons}\nobreak(#1)}
  857. % sequence concatenation
  858. \ifmoremath@
  859.    \mathchardef\sconc="2\mm@63
  860. \else\ifams@
  861.   \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\mathchar"2\msy@79$}}}}
  862. \else
  863.   % this is truly yukky
  864.   \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
  865.     \raise0.2ex\hbox{\it\char"12}}}}
  866. \fi\fi
  867. % distributed concatenation
  868. \newMonadicOperator{\Conc}{dconc}
  869. %----------------------------------------------------------------
  870. %    type equation
  871. \newtoks\@typeName
  872. \def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  873.     \@beginVerticalVDM
  874.     \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
  875.         \@endHorizontalVDM}
  876.     \postTypeHook \vskip\postTypeSkip}}
  877. % restricted type (has invariant)
  878. \def\rtype#1#2#3{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  879.     \@beginVerticalVDM
  880.     \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
  881.         \@endHorizontalVDM}
  882.     \vskip\betweenTypeAndInvSkip
  883.     \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
  884.     \postTypeHook \vskip\postTypeSkip}}
  885. % initialised type
  886. \def\ritype#1#2#3#4{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
  887.     \@beginVerticalVDM
  888.     \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
  889.         \@endHorizontalVDM}
  890.     \vskip\betweenTypeAndInvSkip
  891.     \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
  892.     \vskip\betweenInvAndInitSkip
  893.     \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{#4}%
  894.     \postTypeHook \vskip\postTypeSkip}}
  895. \def\preTypeHook{} \def\postTypeHook{}
  896. \newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
  897. \newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
  898. \newskip\betweenTypeAndInvSkip
  899.   \betweenTypeAndInvSkip=.5ex plus .3ex minus .2ex
  900. \newskip\betweenInvAndInitSkip
  901.   \betweenInvAndInitSkip=.5ex plus .3ex minus .2ex
  902. %----------------------------------------------------------------
  903. %    Composite Objects
  904. % literal composition; we have a compose and a composite env.
  905. % single line compose
  906. \@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
  907. \@namedef{endcomposite*}{\relax$\kw{ end}}
  908. % multiple line version
  909. \def\composite#1{\bgroup\vskip\preCompositeSkip
  910.     \@beginVerticalVDM
  911.     \moveright\VDMindent\vtop\bgroup
  912.     \@beginHorizontalVDM
  913.     \kw{compose }#1\kw{ of}%
  914.     \@endHorizontalVDM
  915.     \@makeColonActive\@changeLineSeparator
  916.     \expandafter\halign\expandafter\bgroup\expandafter\qquad
  917.         \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  918. \def\endcomposite{\crcr\egroup % closes \halign
  919.     \kw{end}\egroup % ends the \vtop
  920.     \vskip\postCompositeSkip\egroup}
  921. \def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}
  922. \newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
  923. \newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex
  924. % record composites; likewise we have a short and a long form
  925. \newtoks\@recordName
  926. \def\record#1{%
  927.   \InvEncountered@false \InitEncountered@false
  928.   \@invTokens={}\@initTokens={}
  929.   \@recordName{#1}
  930.   \par\preRecordHook
  931.   \vskip\preRecordSkip
  932.   \@beginVerticalVDM
  933.   \moveright\VDMindent\hbox\bgroup
  934.       \setbox0=\hbox{$#1$\enspace::\enspace}%
  935.       \@makeColonActive\@changeLineSeparator
  936.       \advance\hsize by-\wd0 \box0
  937.       \@restoreMargins
  938.       % the \expandafters are necessary because TeX doesn't expand
  939.       % \halign specs when scanning for # and &
  940.       \vtop\bgroup\expandafter\halign\expandafter\bgroup
  941.           \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
  942. \def\endrecord{\crcr\egroup% closes halign
  943.     \egroup% closes vtop
  944.     \egroup% closes hbox
  945.   \ifInvEncountered@
  946.     \betweenRecordAndInvHook
  947.       \vskip\betweenRecordAndInvSkip
  948.     \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{%
  949.         \the\@invTokens}
  950.   \fi
  951.   \ifInitEncountered@
  952.     \betweenInvAndInitHook
  953.       \vskip\betweenInvAndInitSkip
  954.     \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{%
  955.         \the\@initTokens}
  956.   \fi
  957.   \par\postRecordHook
  958.   \vskip\postRecordSkip}
  959. \def\inv{\global\InvEncountered@true \global\@invTokens=}
  960. \def\init{\global\InitEncountered@true \global\@initTokens=}
  961. \newif\ifInvEncountered@
  962. \newif\ifInitEncountered@
  963. \newtoks\@invTokens
  964. \newtoks\@initTokens
  965. \def\betweenRecordAndInvHook{}
  966. \def\betweenInvAndInitHook{}
  967. \newskip\betweenRecordAndInvSkip
  968.   \betweenRecordAndInvSkip=0.5ex plus 0.2ex minus 0.1ex
  969. \newskip\betweenInvAndInitSkip
  970.   \betweenInvAndInitSkip=0.5ex plus 0.2ex minus 0.1ex
  971. % the user can decide on the exact alignment of the field names
  972. \newtoks\@recordAlign
  973. \def\leftRecord{\@recordAlign={$##$\hfil}}
  974. \def\rightRecord{\@recordAlign={\hfil$##$}}
  975. \rightRecord
  976. % more catcode trickery
  977. \def\defrecord{\bgroup\@makeColonActive\@defrecord}
  978. \def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}
  979. \newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
  980. \newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
  981. \newcount\preRecordPenalty \preRecordPenalty=0
  982. \newcount\postRecordPenalty \postRecordPenalty=-100
  983. \def\preRecordHook{\penalty\preRecordPenalty }
  984. \def\postRecordHook{\penalty\postRecordPenalty }
  985. % \chg: mu function on composites
  986. \def\chg#1#2#3{\mu(#1,#2\mapsto#3)}
  987. %----------------------------------------------------------------
  988. %    Hooks
  989. % hooked identifiers --- these are taken from the TeXbook, p.357, 359
  990. \ifps@
  991.  \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  992.   \cleaders\hbox{$\mkern-2mu \mathchar"0\cmsy@00 \mkern-2mu$}\hfill
  993.   \mkern-6mu \mathchar"0\cmsy@00$}  % p.357, \leftarrowfill
  994. \else
  995.  \def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  996.   \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
  997.   \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill
  998. \def\overleftharpoonup#1{{%
  999.   \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
  1000.                % for versions after 15 Dec 87
  1001.   \vbox{\ialign{##\crcr % p.359, \overleftarrow
  1002.     \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
  1003.     $\hfil\displaystyle{#1}\hfil$\crcr}}}}
  1004. \let\hook=\overleftharpoonup  % c'est simple comme bonjour
  1005. %-----------------------------------------------------------------
  1006. %     General formula environment, a bit like \[ \] but is
  1007. %    indented to \VDMindent and will take \\
  1008. \def\form#1{\formula #1\endformula}
  1009. \def\formula{\par\preFormulaHook
  1010.     \vskip\preFormulaSkip
  1011.     \@beginVerticalVDM
  1012.     \bgroup
  1013.     \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
  1014. \def\endformula{\@endHorizontalVDM\egroup % ends the vtop
  1015.     \egroup % ends the overall group
  1016.     \par\postFormulaHook
  1017.     \vskip\postFormulaSkip}
  1018. \newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
  1019. \newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
  1020. \newcount\preFormulaPenalty \preFormulaPenalty=0
  1021. \newcount\postFormulaPenalty \postFormulaPenalty=-100
  1022. \def\preFormulaHook{\penalty\preFormulaPenalty }
  1023. \def\postFormulaHook{\penalty\postFormulaPenalty }
  1024. %----------------------------------------------------------------
  1025. %    Formula within a box, when width is unknown
  1026. %    equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
  1027. %        ...\@endHorizontalVDM}
  1028. \def\formbox{\vtop\bgroup\@beginHorizontalVDM}
  1029. \def\endformbox{\strut\@endHorizontalVDM\egroup}
  1030. %----------------------------------------------------------------
  1031. %    special font for constants
  1032. \def\constantFont{\sc}
  1033. \def\const#1{\hbox{\constantFont{#1}\/}}
  1034. %----------------------------------------------------------------
  1035. %    line break and indent
  1036. \def\T#1{\\\hbox to #1em{}}
  1037. %----------------------------------------------------------------
  1038. %    line break and push line after to RHS
  1039. \def\R{\\\hspace*{\fill}}
  1040. %----------------------------------------------------------------
  1041. %    Proofs
  1042. % a proof environment for typesetting proofs in the "natural
  1043. % deduction" style.
  1044. \newdimen\ProofIndent \ProofIndent=\VDMindent
  1045. \newdimen\ProofNumberWidth \ProofNumberWidth=\parindent
  1046. \def\proof{\par\preProofHook
  1047.     \vskip\preProofSkip
  1048.     \let\&=\@proofLine
  1049.     \moveright\ProofIndent\vtop\bgroup
  1050.         \@indentLevel=1
  1051.         \advance\linewidth by-\ProofIndent
  1052.         \begin{tabbing}%
  1053.         \hbox to\ProofNumberWidth{}\=\kill}    % template line
  1054. \def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
  1055.     \egroup % ends the \vtop
  1056.     \par\postProofHook
  1057.     \vskip\postProofSkip}
  1058. \newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
  1059. \newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex
  1060. \newcount\preProofPenalty \preProofPenalty=-100
  1061. \newcount\postProofPenalty \postProofPenalty=0
  1062. \def\preProofHook{\penalty\preProofPenalty }
  1063. \def\postProofHook{\penalty\postProofPenalty }
  1064. \def\From{\@indentProof\kw{from }\=%
  1065.     \global\advance\@indentLevel by 1
  1066.     \@enterMathMode}
  1067. \def\Infer{\global\advance\@indentLevel by-1
  1068.     \@indentProof\kw{infer }\@enterMathMode}
  1069. \def\@proofLine{\@indentProof\@enterMathMode}
  1070. \def\by{\`}
  1071. \newcount\@indentLevel
  1072. \newcount\@indentCount
  1073. \def\@indentProof{% do \>, \@indentLevel times
  1074.     \global\@indentCount=\@indentLevel
  1075.     \@gloop \>\global\advance\@indentCount by-1
  1076.     \ifnum\@indentCount>0
  1077.     \repeat}
  1078. % need special loop macros that works in across boxes
  1079. \def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
  1080. \def\@giterate{\@body \global\let\@gloopNext=\@giterate
  1081.     \else \global\let\@gloopNext=\relax \fi \@gloopNext}
  1082. % this enters math mode and sets the LaTeX macros \@stopfield up
  1083. % to exit math mode
  1084. \def\@enterMathMode{\def\@stopfield{$\egroup}$}
  1085. %----------------------------------------------------------------
  1086. \def\VDMauthor{M.Wolczko,
  1087. CS Dept.,
  1088. Univ. of Manchester, UK.
  1089. mario@cs.man.ac.uk
  1090. uknet!man.cs!mario}
  1091. \def\VDMversion{vdm3.0}
  1092. \typeout{BSI VDM style option <1 May 1992>}
  1093. %----------------------------------------------------------------
  1094. %    Global changes
  1095. % All things that have to be invoked before the user's stuff appears
  1096. % should go here.
  1097. % by default the math spacing and changes to @ and _ apply everywhere
  1098. \@changeOtherMathcodes \@changeGlobalCatcodes
  1099. %-------------------the end--------------------------------------
  1100. \endinput
  1101. %    Summary of penalties
  1102. %    Penalties in vertical mode
  1103. % \preOperationPenalty        before an op begins
  1104. % \preExternalPenalty        between the header and externals of an op
  1105. % \prePreConditionPenalty    before the precondition
  1106. % \prePostConditionPenalty    before the postcondition
  1107. % \postOperationPenalty        at the end of an op
  1108. % \preFunctionPenalty        before a fn begins
  1109. % \betweenSignatureAndBodyPenalty -guess
  1110. % \postFunctionPenalty        after a fn ends
  1111. % \preRecordPenalty        before a record
  1112. % \postRecordPenalty        after a record
  1113. %    etc for formula, proof
  1114. %    Penalties in horizontal mode in boxes
  1115. % \linepenalty            101        \@raggedRight
  1116. % `if mm-exp ^ then..'        0        \SIf
  1117. % `if ... then mm-exp ^ else'    -100        \SIf
  1118. % `let mm-exp in ^ ...'        -100        \SLet
  1119. % `map mm-exp ^ to ...'        -50        \map
  1120. % ^\iff                -50        \iff
  1121. % ^\implies            -35        \implies
  1122. % func(args) \DEF^        -100        \begin{fn}
  1123. % \binoppenalty            10000
  1124. % \relpenalty            10000
  1125. % \hyphenpenalty        -100        \suchthat
  1126. % ^\to                -100        \to
  1127. % _^                100        \@VDMunderscore
  1128.